{-
    Copyright © 2011 - 2021, Ingo Wechsung
 
    All rights reserved.
 
    Redistribution and use in source and binary forms, with or
    without modification, are permitted provided that the following
    conditions are met:

    -   Redistributions of source code must retain the above copyright
        notice, this list of conditions and the following disclaimer.

    -   Redistributions in binary form must reproduce the above
        copyright notice, this list of conditions and the following
        disclaimer in the documentation and/or other materials provided
        with the distribution. Neither the name of the copyright holder
        nor the names of its contributors may be used to endorse or
        promote products derived from this software without specific
        prior written permission.
 
    *THIS SOFTWARE IS PROVIDED BY THE
    COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR
    IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
    WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
    PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER
    OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
    SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
    LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF
    USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED
    AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
    LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING
    IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF
    THE POSSIBILITY OF SUCH DAMAGE.*
-}

{--
    This package provides classes and functions that deal with the lesser pure
    parts of Frege - Exceptions, Threads, mutable data.
    
    This package is _implementation specific_ insofar as the compiler may
    assume that certain items are defined here in a certain way.
    Changes may thus lead to compiler crashes or java code that 
    will be rejected by the java compiler.
    
    In particular, derived 'Exceptional' instances will reference
    type class 'Exceptional'.
    
 -}


protected package frege.prelude.PreludeIO where

import frege.prelude.PreludeBase
import frege.prelude.PreludeMonad
import frege.control.Semigroupoid


infixl 2 catch finally

-- ########################## Wrapped Exceptions ############################################
native module where {

}

{-- 
    Make the @java.lang.Class@ object corresponding to the instantiated type available.
    
    An instance for this type class is needed for the element type 
    of 'frege.prelude.PreludeArrays#JArray's 
    (which are based on 
    'http://docs.oracle.com/javase/7/docs/api/java/lang/reflect/Array.html reflective true Java arrays')
    one needs to create.
    
    A subclass of this is 'Exceptional' which
    adds no additional functionality and behaves
    basically just as a marker interface for exceptions.
         
    'JavaType' instances are derivable for all data types.
    -}                                
    
class JavaType e where
    --- The @java.lang.Class@ object of the instantiated type
    javaClass  :: Class e


{-- 
    Function 'catch' requires that the argument of a handler function
    is an instance of 'Exceptional'. 

    This is derivable for @pure@ @native@ data types.
    -}

class JavaType e => Exceptional e 

derive Exceptional Undefined
derive Exceptional NoMatch
derive Exceptional GuardFailed

protected data Exception = pure native java.lang.Exception
derive Exceptional Exception

--- nowarn: argument of type (ST s a)
--- Runtime method for implementation of 'catch'
protected native doCatch PreludeBase.WrappedCheckedException.doCatch {}
                :: Class b -> ST s a -> (b -> ST s a) -> ST s a
{--
    The construct
    
    > action `catch` handler
    
    is a 'ST' action with the same type as _action_.
    
    If _action_ yields a result, this will be the result of the overall action.
    However, if, during execution of _action_ the JVM raises an exception _e_ with 
    java type @E@, and @E@ is a subtype of java type @H@, and @H@ is the 
    java type associated with the argument of _handler_, the return value will be:
    
    > handler e
    
    Otherwise, if the type of _e_ does not allow to pass it to _handler_ it will
    be propagated upwards and @a `catch` b@ will not return to its caller.
    
    Because 'catch' is left associative, it is possible to catch different exceptions,
    like in:
    
    > action `catch` handler1 `catch` handler2
    
    Care must be taken to check for the *most specific* exception first. In the example above,
    if the exception handled by _handler1_ is *less specific* than the one handled by _handler2_,
    then _handler2_ will never get a chance to execute. 
    
    Another way to put this is to say that if @E1@ and @E2@ are distinct exception types
    handled in a chain of 'catch'es, and @E1@ is (from the point of view of Java!) a
    subtype of @E2@, then the handler for @E1@ must appear further left than the handler for
    @E2@. If it is a super type of @E2@, however, its handler must appear further right.
    And finally, if the types do not stand in a sub-type relationship, the order of the 
    handlers is immaterial.
    
    *Note* If _action_ is of the form:
    
    > doSomething arg
    
    then, depending on the strictness of _doSomething_ the argument _arg_ may be evaluated
    *before* the action is returned. Exceptions (i.e. undefined values) 
    that occur in the construction of the action do *not* count as 
    exceptions thrown during execution of it, and hence cannot be catched.
    
    Example:
    
    > println (head []) `catch`  ....
    
    will not catch the exception that will be thrown when println evaluates  
    
    For a remedy, see 'try'.         
    -}
catch ∷ Exceptional γ ⇒ ST β α → (γ→ST β α) → ST β α
catch action handler = doCatch javaClass action handler

--- nowarn: argument of type (ST s a)
{--
    The construct
    
    > action `finally` always
    
    returns the same value as _action_, when executed.
    
    However, no matter if _action_ produces a value or diverges 
    (for example, by throwing an exception), in any case will _always_ be executed,
    and its return value dismissed.
    
    Note that 'finally' only returns to its caller if _action_ would have done so.
    
    'finally' has the same fixity as 'catch', hence it is possible to have
    
    > action `catch` handler1 `catch` handler2 `finally` always
    
    -}
native finally PreludeBase.WrappedCheckedException.doFinally{}  :: ST s a -> ST s b -> ST s a

private native throwRT PreludeBase.WrappedCheckedException.throwST 
    :: PreludeBase.Throwable -> ST s ()

--- Deliberately throw an exception in the 'ST' monad.
throwST  :: PreludeBase.Throwable -> ST s a
throwST ex = throwRT ex >> pure undefined

--- Deliberately throw an exception in the 'IO' monad.
throwIO :: PreludeBase.Throwable -> IO a
throwIO ex = throwRT ex >> pure undefined

{--
    Make sure that exceptions thrown during construction of an action can be catched.
    See 'catch' for an explanation.
    
    Example:
    
    > try println (head []) `catch` (\u::Undefined -> println u.catched)
    
    should print:
    
    > frege.runtime.Undefined: Prelude.head []
    
    'try' does work for unary functions only. 
    To be safe with functions taking more actions, use:
    
    > pure a >>= (\a -> pure b >>= (\b -> f a b))
    -}
try f a = pure a >>= f

{--
    The 'catchAll' function runs a 'ST' action and returns 
    either the result or the exception thrown.
-}
catchAll :: ST α β -> ST α (Exception | β)
catchAll sta = sta >>= pure . Right `catch` (\(t::Exception) -> pure (Left t))

-- -------------------------------------------------------------------------
--          Mutable Native Data Types
-- -------------------------------------------------------------------------

{--
    'Mutable' is a wrapper for native data types. 
    A value of type @Mutable s x@ is really an @x@, but it is tied to the 'ST' thread s,
    from which it cannot escape.
    
    The compiler will enforce the following rules:
    
    1. When type checking @x.m@ and @(x::Mutable s T)@, @m@ will be searched in the namespace @T@
    2. An impure native method must only take and return @Mutable s T@, unless @T@ is
       itself *@pure@* (of course, all algebraic data types are pure)
    3. A pure type @T@ must not appear as @Mutable s T@ in native functions.
    4. Pure native functions may not return @Mutable s t@ for any @t@.
    5. Pure native functions must not normally get arguments of type @Mutable s T@. (see below)
    6. In a type of the form @ST x (Mutable y d)@, it will be enforced that _x_ is the same
       type as _y_. Furthermore, all phantom types of all 'Mutable' types must be the same
       in a type signature.
    
    To understand the motivation for rule 5, observe that the 'Mutable.Mutable' 
    data constructor cannot be applied in Frege code, hence the only possibility 
    to obtain a value of type @Mutable s t@  is through a native function. 
    But by rule 4 above, this could only happen in the 'ST' or 'IO' monad, 
    from whence those values cannot escape. The 'ST' monad is a context where
    the sequence of actions matters. If we allowed passing mutable data to pure
    functions, their results would depend on whether 'ST' actions modified the 
    value before the result is actually evaluated.
    
    Although in a strict sense, no pure function should get mutable data, rule 5 is only
    enforced for native pure functions, as normal frege functions couldn't do anything
    with the native value, except passing them on to native functions eventually.
    
    There will be means to get a read-only copy ('freeze') of a mutable value through
    class 'Freezable'.
    
    There is also the possibility that, although a value is mutable, 
    there are certain properties that cannot change (such as the length of an array). 
    It will be possible to bypass rule 5 in such cases.
    
    To summarize:
    
    - Mutable data live in the 'ST' or 'IO' monad, from which they cannot escape.
    - They can be passed only to other 'ST' actions that operate in the same state thread,
      as indicated by the phantom type, that is either a type variable or 'RealWorld'.
    - Read only copies of mutable values and mutable copies of read-only values can be obtained.        
    - Rule 5 can be bypassed in exceptional cases.

    *Implementation note:* It is assumed that 'Mutable' is a *@newtype@*.
    -}
abstract newtype Mutable (s :: *) m = Mutable m where
    --- obtain a read-only copy of a mutable value through cloning or serialization.
    freeze :: Freezable m => Mutable s m -> ST s m
    freeze (Mutable x) = pure (Freezable.freeze x)
    
    --- obtain a mutable copy of a read only value through cloning or serialization.
    thaw :: Freezable m => m -> ST s (Mutable s m)
    thaw = pure . Mutable . Freezable.thaw 
    
    --- Apply a pure function to a mutable value that pretends to be read-only.
    --- The function must not rely on anything that could change in the mutable data!
    readonly :: (m -> b) -> Mutable s m -> ST s b 
    readonly f (Mutable x) =  pure (f x)

--- Apply a pure function to a mutable value that pretends to be read-only.
--- The function must not rely on anything that could change in the mutable data!
readonly  = Mutable.readonly

--- Obtain a read only native value (temporarily) typed as 'Mutable'
{-- 
    For example, this could be needed when running a native 'ST' method
    that uses the value as read-only, but we can't declare it, like:

    > private native copyOf java.util.Arrays.copyOf 
    >               :: ArrayOf s HashMap -> Int -> ST s (ArrayOf s HashMap)
-}
mutable x = Mutable.Mutable x
 

--- The type for mostly mutable values that are tied to the 'IO' monad.
type MutableIO = Mutable RealWorld

--- The type of 'IO' actions that return a mutable value of type _d_
--- This is an abbreviation for @ST RealWorld (Mutable RealWorld d)@ 
type IOMutable d = IO (MutableIO d)

--- The type of 'ST' actions that return a mutable value of type _d_
--- This is an abbreviation for @ST s (Mutable s d)@ 
type STMutable s d = ST s (Mutable s d)


{--
 * Type class for mutable values that support making read-only copies.
 * To be implemented with care.
 -}
class Freezable f where
    {--
     * "Freeze" a mutable native value. The result is supposed to be immutable
     * or at least not reachable from other parts of the code, especially from java code.
     *
     * The most prominent way to freeze a value is by 'clone'-ing it, if that is supported.
     * But note that sometimes a deep copy would be needed, and that @clone@ does not do that.
     -}
    protected freeze :: f -> f
    {--
     * The inverse of 'freeze' creates a value (an object) which can be passed
     * to impure functions without compromising the frozen object passed as argument.

     * One possibility to thaw an object is by cloning it.

     * If 'thaw' is not implemented correctly, bad things may happen.

     -}
    protected thaw   :: f -> f




{--
 * For a data type declared like
 * > data D = native Javatype
 * where @Javatype@ implements the @java.lang.Cloneable@ interface,
 * one can get implementations for 'Freezable.freeze'
 * and 'Freezable.thaw' by just stating
 * > instance Cloneable D
 * The 'freeze' and 'thaw' operations are implemented in terms of 'clone'.
 *
 * Note: Cloning does *not* produce safe copies if the cloned object
 * contains references to mutable objects. In such cases, sort of a deep cloning
 * would be required.
 -}
class (Freezable f) => Cloneable f  where
    {--
     *  @clone v@ must be a native method that works like @java.lang.Object#clone@.
     -}
    pure native clone :: f -> f 
    freeze x = clone x
    thaw   x = clone x

{--
 * For a data type declared like
 * > data D = native Javatype
 * where @Javatype@ implements the @java.io.Serializable@ interface,
 * one can get implementations for 'freeze'
 * and 'thaw' by just stating
 * > instance Serializable D
 * The 'freeze' and 'thaw' operations are implemented in terms of 'copySerializable',
 * which serializes its argument to a byte array and creates a new copy by
 * deserializing it from the byte array.
 -}
class (Freezable f) =>  Serializable f  where
    {--
     *  @copySerializable v@ is supposed to be a native function that is
     *  implemented by @frege.runtime.Runtime.copySerializable@ at the instantiated type.
     -}
    pure native copySerializable frege.runtime.Runtime.copySerializable {} :: f -> f
    --- make a safe copy through serialization/deserialization
    freeze x = copySerializable x
    --- make a safe copy through serialization/deserialization
    thaw   x = copySerializable x


-- ########## Variables ###########################

--- A mutable reference, suitable for use in the 'ST' monad.
data Ref a = native frege.runtime.Ref {a} where
    --- create a reference that is initially set to the argument value 
    native new         :: a -> STMutable s (Ref a)
    --- get the value the reference is pointing to
    native get         :: Mutable s (Ref a) -> ST s a
    --- assign another value to the reference 
    native put         :: Mutable s (Ref a) -> a -> ST s ()
    --- modify the referenced value with a function
    modify r f = do
        item <- get r
        put r (f item) 

--- Haskell compatibility
type IORef a = MutableIO (Ref a)
readIORef    = Ref.get
writeIORef   = Ref.put
modifyIORef  = Ref.modify
newIORef     = Ref.new
